$\forall$$T$:Type, $L$:($T$ List), $R$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow$es\_realizer\{i:l\}), $A$:es\_realizer\{i:l\}.
\\[0ex]R{-}compat\{i:l\}($A$; Rall($L$; $x$.$R$($x$))) $\Leftarrow\!\Rightarrow$ ($\forall$$x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ R{-}compat\{i:l\}($A$; $R$($x$)))